p,q,a,b:.
coprime(p; q)
 coprime(a; b)
 ((p * b) = (a * q))
 ((p < 0)  (a < 0))
 ((q < 0)  (b < 0))
 guard(((p = a)  (q = b))) 

latex

Definitions	P  Q, gcd_p(a; b; y), coprime(a; b), P  Q, P  Q, guard(T), sq_type(T), x:A. B(x), divides(b; a), assoced(a; b), P  Q, prop{i:l}, t  T, P  Q, x:A. B(x), False, A, decidable(P)
Lemmas	iff wf, decidable lt, assoced elim, assoced wf, and functionality wrt iff, divides wf, mul add distrib, mul com, coprime bezout id, coprime wf